p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))).
rv-iid(p;n.f(n);n.X(n))
 (E(f(0);X(0)) = 0  )
 nullset(p;s.q:. (0 < q & (n:. m:. ((n < m) & q  |0  i < m. (1/m) * (X(i)(s))|)))) 

latex

Definitions	t  T, x:A. B(x), A  B, , {x:A| B(x)} , FinProbSpace, x:AB(x), measure(C)  q, s  C, nullset(p;S), s = t, a < b, rv-disjoint(p;n;X;Y), , x:A  B(x), P & Q, i  j < k, {i..j}, Void, P  Q, False, A, <a, b>, , A c B, f(a), x. t(x), rv-identically-distributed(p;n.f(n);i.X(i)), rv-iid(p;n.f(n);i.X(i)), , r < s, r  s, x:A. B(x), RandomVariable(p;n), Type, #$n, x(s), r * s, (x.F(x)) o X, E(n;F)
Lemmas	slln-lemma3, finite-prob-space wf, random-variable wf, int inc rationals, rv-iid wf, nat wf, int-rational, expectation wf, rv-compose wf, qmul wf, rationals wf, le wf